COMMENT ⊗   VALID 00017 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00003 00002	\section{Some simple examples of proofs}
C00026 00003	\section{Pattern matching}
C00030 00004	{\bf The programs /sublis/ and /match/}
C00034 00005	{\bf Some simple properties of /match/}
C00036 00006	\noindent{\bf Proposition 1:} If $\alpha \in \qAl{subst}$ then 
C00040 00007	The next proposition shows that /match/ is in some sense an /increasing/
C00043 00008	The next result shows that $/match/[x,\ y,\ \alpha]$ and any extension of it
C00048 00009	\noindent{\bf Correctness of /match/}
C00053 00010	So far we have proved that if /match/ is successful then it does what we want it to
C00058 00011	\section{Unification}
C00062 00012	\noindent{\bf Theorem 3:}
C00072 00013	The fact that /unify/, when it succeeds, does what we want it to do 
C00077 00014	The fact that /unify/ does indeed succeed whenever it can is the task of the next
C00086 00015	As a simple application of the previous theorem we can prove that
C00091 00016	The following we leave as an exercise for the student. it is a quite straight
C00092 00017	\noindent{\bf A more efficient unification program:}
C00094 ENDMK
C⊗;
\section{Some simple examples of proofs}
\sectlab{simple}

In this section we shall prove some simple properties of some simple 
programs. Our first example deals with the program /append/. As promised
in \sectref{adding funs} we begin by proving:

\noindent{\bf Proposition:} $\forall X\ [X\qapp y \not=\bot \liff X\in \qL!]$

We restate the definition of /append/ here for the readers convenience.
$$x\qapp y \leftarrow \qif \qn x \qthen y \qelse \qa x \qcons [\qd x \qapp y]$$

\noindent{\bf Proof:} By the bottom axiom for the function \qapp\ we know that
$\bot\qapp y=\bot$, and as $\bot\not\in\qS!$ we know that $\bot\not\in\qL!$.
What remains for us to prove is that 
$$\forall x\ [x\qapp\ y \not= \bot \liff x\in\qL!]$$
which we prove by induction on the rank of $x$, our rank function being
$r↓{sexp}$ and $\Phi[x]$ being
$$x\qapp\ y \not= \bot \liff x\in\qL!.$$

To prove $\forall x\Phi[x]$,which is our aim, we need only prove
$$\forall x[\forall y[[r(y)<r(x)]\supset \Phi[y]] \supset \Phi[x]].$$
 In other words we must prove, for each $x\in\qS!$  that the assumption
$$\forall y[[r(y)<r(x)]\supset \Phi[y]] \supset \Phi[x]$$
(often called the /induction/ /hypothesis/) implies
$$\Phi[x].$$
It is at this point that we split the proof into two cases. The first case
corresponds to when $x$ is of least rank, in which case the induction hypothesis
is trivially true and so not of much use. The second case then is when $x$ is
not of least rank. Since we are using the rank function $r↓{sexp}$ these cases
correspond to when $x\in\qA!$ and when $x\in\qC!$.

\noindent{\bf Base case:} $r↓{sexp}(x)=0$, or in clearer terms $x\in\qA!$. By the 
program axiom for append we have
$$x\qapp y = \qif \qn x \qthen y \qelse \qa x \qcons [\qd x \qapp y]$$
and we also have the two possibilities, either $x=|NIL|$ or $x\not=\qNIL$.

In the former case
$$x\qapp y = \qif \qT \qthen y \qelse \qa x \qcons [\qd x \qapp y]$$
by the null axiom, and now by the if axiom we have
$$x\qapp y = y$$

In the later case we have 
$$x\qapp y = \qif \qNIL \qthen y \qelse \qa x \qcons [\qd x \qapp y]$$
by the null axiom, so by the if axiom we have
$$x\qapp y = \qa x \qcons [\qd x \qapp y]$$
but by the car axiom we know $\qa x = \bot$ so this becomes
$$x\qapp y = \bot \qcons [\qd x \qapp y]$$
and consequently by the cons axiom
$$x\qapp y = \bot$$

Thus we have proved that when $x$  is an atom then
$$x=\qNIL \supset x\qapp y\not= \bot$$
$$x\not=\qNIL \supset x\qapp y= \bot$$

Now since
$\qL! = \{|NIL|\} \cup [ \qS! \times \qL!]$ and
$\qS!\times\qL! \subset \qC!$ by the mapping equations, the above is simply
$$x\qapp\ y \not= \bot \liff x\in\qL!.$$
$\qed↓{\bf base\ case}$

\noindent{\bf Induction step:} Suppose $x\in\qC!$ and assume the induction hypothesis,
namely,
$$\forall y[[r(y)<r(x)]\supset \Phi[y]] \supset \Phi[x]$$

Firstly observe that by the definition of \qL! we have, in this case,
$$x\in\qL! \liff \qd x\in\qL!$$
Now since $r↓{sexp}(\qd x)<r↓{sexp}(x)$ we can use the induction hypothesis
to conclude 
$$\qd x\qapp\ y \not= \bot \liff \qd x\in\qL!.$$

Finally since $x\in\qC!$ we have that $\qa x \not=\bot$ and so by the cons axiom 
we know that
$$\qa x\qcons[\qd x \qapp y]= \bot \liff  \qd x \qapp y = \bot$$
and using the program axiom we have 
$$x\qapp y = \qa x \qcons [\qd x \qapp y]$$
and putting all these equivalences together gives us the desired conclusion
$$x\qapp\ y \not= \bot \liff x\in\qL!.$$
$\qed↓{\bf induction\ step}$

Putting the base case and the induction step together shows that for every
$x\in\qS!$
$$\forall x[\forall y[[r(y)<r(x)]\supset \Phi[y]] \supset \Phi[x]].$$
and so by the rank induction principle we conclude
$$\forall x \Phi[x]$$
$\qed↓{\bf proposition}$
We shall now prove some algebraic properties of /append/. Not surprisingly
most of the nice properties of /append/ are only true when the function
is restricted to \qL!. In fact a simple elaboration of the last proof will show
that \qapp\ is an operation on \qL!:

\exercise $\qapp\ : \qL!\times\qL! \to\qL!$

Our first simple property expresses the fact that  |NIL| is both the left and
the right identity of the operation \qapp\ .

\noindent{\bf Proposition:} $|NIL|\qapp u = u\qapp|NIL| = u$

\noindent{\bf Proof:} The fact that $|NIL|\qapp u = u$ follows simply from the 
program, null and if axioms, since

$|NIL|\qapp u$

$= \qif \qn |NIL| \qthen u \qelse \qa |NIL| \qcons [\qd |NIL| \qapp u]$

$= \qif \qT \qthen u \qelse \qa |NIL| \qcons [\qd |NIL| \qapp u]$

$= u$

In future we shall not write out these simple reductions in such detail since
they become quite tedious, time consuming and they detract from the
essential points in the argument.

Now we prove the second part of the proposition, that
$$u\qapp |NIL| = u$$
We prove this by the /relativised/ /rank/ /induction/ /schema/ 

\noindent{\bf Rank Induction:}  $\forall u[\forall v[[r(v)<r(u)]\supset \Phi[v]] \supset
\Phi[u]] \supset \forall u \Phi[u]$

\exercise Prove that the relativized rank induction shema follows from the usual one.

 We prove by induction
on the rank of u, where the rank function is $r↓{list}$, that
$\forall u \Phi[u]$ where $\Phi[u]$ is simply
$$u\qapp |NIL| = u.$$

\noindent{\bf Base case:} In this case $r↓{list}(u)=0$ so $u=|NIL|$ and $\Phi[|NIL|]$
follows from the previous case.
$\qed↓{\bf base\ case}$

\noindent{\bf Induction step:} Suppose that $r↓{list}(u)>0$ ( i.e $u\in\qL{non-empty}$)
and that $\Phi [v]$ is true 
for all lists of less rank than $u$. In other words
$$\forall u[\forall v[[r(v)<r(u)]\supset \Phi[v]] \supset \Phi[u]]$$
then
$$u\qapp |NIL| = \qa u \qcons[ \qd u \qapp |NIL|]$$
by the if and null axioms.
But by the induction hypothesis $\qd u \qapp |NIL| = \qd u$ so we have
$$u\qapp |NIL| = \qa u \qcons  \qd u $$
and this is just $u$ by the cons axiom.
$\qed↓{\bf induction\ step}$

So we have shown that $\Phi[|NIL|]$ is true and that assuming the induction
hypothesis $\Phi[u]$ is true for all $u\in\qL{non-empty}$ thus we may conclude
$$\forall u \Phi[u]$$
$\qed↓{\bf proposition}$
We now prove that the append operation is associative. Thus showing that
the set \qL! together with the operation \qapp\ forms  what mathematicians call
a semigroup with identity.

\noindent{\bf Proposition:}
$\forall u,v,w\ u\qapp[v\qapp w] = [u\qapp v]\qapp w$

\noindent{\bf Proof:} Pick any $v,w\in \qL!$, we will show by induction on $r↓{list}(u)$ that
$$\forall u\ u\qapp[v\qapp w] = [u\qapp v]\qapp w$$
with $\Phi[u]$ being
$$u\qapp[v\qapp w] = [u\qapp v]\qapp w$$

\noindent{\bf Base  case:} $r↓{list}(u)=0$,i.e $u =|NIL|$ . This case is trivial since
$$u\qapp [v\qapp w] =
|NIL|\qapp[v \qapp w] =
[v \qapp w] =
[|NIL|\qapp v] \qapp w $$
by the previous proposition. $\qed↓{base\ case}$

\noindent{\bf Induction step:} In this case $u \in \qL{non-empty}$ and
assume that $\Phi[u↓0]$ holds for all lists $u↓0$ less than $u$. Then
$$u\qapp[v\qapp w] = \qa u \qcons [\qd u \qapp [v\qapp w]]$$
and by the induction hyputhesis
$$\qd u\ \qapp[v\qapp w] = [\qd u\qapp v]\qapp w]$$
so we have
$$u\qapp[v\qapp w] = \qa u \qcons[[\qd u \qapp  v]\qapp w]$$
Now we need the lemma

\noindent{\bf Lemma:} 
$\forall x,u,v\  x \qcons [u \qapp v] = [x \qcons u]\qapp v$

Leaving aside the proof of the lemma for a moment, we can use it immediately to 
obtain
$$u\qapp[v\qapp w] = [\qa u \qcons [\qd u \qapp  v]]\qapp w $$
and again to get
$$u\qapp[v\qapp w] =[[\qa u \qcons  \qd u] \qapp  v]\qapp w $$
but this is just
$$u\qapp[v\qapp w] =[u \qapp  v]\qapp w $$
$\qed↓{\bf induction\ step}$

We finish of the proof of the proposition by proving the lemma.

\noindent{\bf Proof of lemma:} Pick any $x,u,v$ then
$$[x \qcons u]\qapp v= \qa [ x\qcons u] \qcons [\qd[x\qcons u]\qapp v]$$
which reduces to
$$[x \qcons u]\qapp v=  x \qcons [ u\qapp v]$$
$\qed↓{\bf lemma\ and\ theorem}$

  The algebra of this proof is rather typical. 
We used the definition of the function involved several times, 
we used the induction hypothesis once, 
and we used the elementary algebraic facts about conditional
expressions and the basic functions of \lisp.
Also in this proof it does not matter whether we take $\Phi[u]$ to be
$u*[v\qapp w]=[u\qapp v]\qapp w$ or
$\forall v,w\ u*[v\qapp w]=[u\qapp v]\qapp w$   .
 The difference being that
in the first case the induction hypothesis is only refers to the particular
$v$ and $w$ of the conclusion while in the second case it applies to any
lists $v$, $w$.  When proving properties of recursively defined functions,
the unquantified form of $\Phi$ is generally good enough when the 
function definion does not modify the parameters (non-recursion arguments) in
recursive calls.  If it passes functions of the parameters in recursive
calls then it may be necessary to use the quantified version of $\Phi$.
In the next lemma we will need a quantified version.

The next few examples deal with the behavior of /reverse/, /reverse1/ and
/append/.
Recall that /reverse1/ and /reverse/ were defined by the programs.

$$/reverse1/[x] \leftarrow \qif \qn x \qthen |NIL| \qelse reverse1[\qd x]\qapp <\qa x>$$
$$/reverse/[x] \leftarrow /rev/[x,|NIL|]$$
$$rev[x,y]\leftarrow \qif \qn x \qthen y \qelse rev[\qd x, \qa x\qcons y]$$

We restrict our attention to the behaviour of these functions on \qL! because
of the following straightforward after reading the proof of the main lemma
below.
\exercise Show that $\forall x [/reverse/[x]\not=\bot\liff x\in\qL!]$
\exercise Show that $\forall x [/rev/[x,y]\not=\bot\liff x\in\qL!]$
and that $rev : \qL!\times\qL!\to\qL!$
\exercise Show that $\forall x [/reverse1/[x]\not=\bot\liff x\in\qL!]$

We said in \chapref{readin} that the functions /reverse/ and /reverse1/ were the
same. Our first task will be be to prove this fact

\noindent{\bf Proposition:} $\forall u\  /reverse/[u] = /reverse1/[u]$

Before we begin the proof of  this proposition we must prove a property concerning
/rev/. Notice that the previous exercises imply that we actually have
$\forall X\  /reverse/[X] = /reverse1/[X]$.

\noindent{\bf Main Lemma:} For all lists $u$ and $v$ we have that
$$/rev/[u,v]=/rev/[u,|NIL|]\qapp v.$$

\noindent{\bf Proof of Lemma:} The proof of this is by induction on $r↓{list}(u)$ with
$\Phi[u]$ being 
$$\forall v\ /rev/[u,v]=/rev/[u,|NIL|]\qapp v.$$
The base case is overly simple so we only prove the induction step. So 
suppose that $u\in \qL{non-empty}$ and that $\Phi$ holds for lists of less
length (since this is what $r↓{list}$ measures).
Then

$rev[u,v]=\qif \qn u \qthen v \qelse rev[\qd u, \qa u\qcons v]$

and so

$= rev[\qd u, \qa u\qcons v]$

which by the induction hypothesis becomes

$= rev[\qd u, |NIL|]\qapp [\qa u\qcons v]$.

Now by the lemma in the proof of the associativity of /append/ we have
$$\qa u \qcons v  = \qa u \qcons[|NIL|\qapp v] = <\qa u>\qapp v$$
and so we have

$= rev[\qd u, |NIL|]\qapp [<\qa u>\qapp v]$

which by associativity of append and the above exercise showing that
$$rev : \qL!\times\qL!\to\qL!$$

$= rev[\qd u, |NIL|]\qapp  <\qa u>] \qapp v]$

which by the induction hypothesis is just

$= rev[\qd u, <\qa u>]\qapp   v$

and this reduces to

$= rev[\qa u\qcons \qd u, |NIL|]\qapp   v  = rev[u, |NIL|]\qapp   v$

$\qed↓{\bf main\ lemma}$

The proof of the equivalence of /reverse/ and /reverse1/ is now quite simple.

\noindent{\bf Proof of Proposition:}  Is by induction on $r↓{list}(u)$, the base case is
again unproblematic so we content ourselves with the induction step.
Suppose $u\in\qL{non-empty}$ and that
$/reverse/[v] = /reverse1/[v]$ for all lists $v$ of less length.
then

$/reverse/[u]=/rev/[u,|NIL|]$

which is

$=/rev/[\qd u,\qa u \qcons |NIL|]$

$=/rev/[\qd u,<\qa u>]$

which by the main lemma is just

$=/rev/[\qd u, |NIL|]\qapp <\qa u>$

which by definition is

$=/reverse/[\qd u]\qapp <\qa u>$

and using the induction hypothesis we get

$=/reverse1/[\qd u]\qapp <\qa u>$

which by definition is just

$=/reverse1/[u]$

$\qed↓{\bf proposition}$

The next proposition is a fundamental relation between append and reverse.

\noindent{\bf Proposition:}
$\forall u,v\ /reverse/[u\qapp v] =/reverse/[v]\qapp /reverse/[u]$

\noindent{\bf Proof:} Is by induction on the length of $u$, in other words
by induction on $r↓{list}(u)$. $\Phi[u]$ being
$$/reverse/[u\qapp v] =/reverse/[v]\qapp /reverse/[u]$$
As in the previous propositions the base case is very simple so we only
do the induction step. So suppose that $u\in\qL{non-empty}$ and that $\Phi$
holds for all lists of less length. Then

$/reverse/[u\qapp v] =/rev/[u \qapp v, |NIL|]$

which using the definition is

$=/rev/[\qd [u \qapp v], <\qa[u \qapp v]>]$

but $\qa [u \qapp v] = \qa u$ and $\qd [u \qapp v] = \qd u\qapp v$, so

$=/rev/[\qd u \qapp v, <\qa u>]$

which by the main lemma is

$=/rev/[\qd u \qapp v, |NIL|]\qapp <\qa u>$

using the induction hypothesis we get

$=[/reverse/[v]\qapp /reverse/[\qd u]]\qapp <\qa u>$

which by associativity is

$=/reverse/[v]\qapp [/reverse/[\qd u] \qapp <\qa u>]$

using the definition this is

$=/reverse/[v]\qapp [/rev/[\qd u, |NIL|] \qapp <\qa u>]$

which again using the lemma is

$=/reverse/[v]\qapp /rev/[\qd u, <\qa u>]$

and resorting to the definition once more

$=/reverse/[v]\qapp /rev/[\qa u\qcons \qd u, |NIL|]$

$=/reverse/[v]\qapp/reverse/[u]$

$\qed↓{proposition}$

The final property we prove of /reverse/ is that it is its own inverse.

\noindent{\bf Proposition:}
$\forall u\ /reverse/[/reverse/[u]]=u$

\noindent{\bf Proof:} The proof is a simple corollary of the previous proposition.
we again prove it by induction of the length of $u$. Noting that the base case
is immediate. So suppose that $u\in\qL{non-empty}$  and the proposition is true for
all lists of less length.
The crucial observation is that $u = <\qa u>\qapp \qd u$ and so

$/reverse/[/reverse/[u]]=/reverse/[/reverse/[<\qa u>\qapp \qd u]]$

which by the previous proposition is just

$=/reverse/[/reverse/[\qd u]\qapp /reverse/[<\qa u>]]$

which again by the previous proposition is 

$=/reverse/[/reverse/[<\qa u>]]\qapp/reverse/[/reverse/[\qd u]]$

but by the induction hypothesis this is just

$=<\qa u> \qapp \qd u = \qa u \qcons \qd u =u$

$\qed↓{proposition}$
\section{Pattern matching}
\sectlab{pattern}

        In this section we will solve a pattern matching problem and prove the
correctness of our program. The point being to give an example of a solution to a real
programing problem, whose correctness proof is non-trivial.

        Pattern matching is an fundamental issue in  computer science so we shall
not waste time here espousing its importance, but rather describe the particular
problem that we wish to solve. Suppose we have an S-expression $x$ that contains
certain atoms that we shall call {\it pattern variables}, their nature is 
unimportant at the moment . The problem that we wish to solve is the following:
        Given another S-expression $y$ can we match the pattern variables   that
occur in $x$ with subexpressions of $y$ in such a fashion that the result of
uniformly substituting the occurrences of the pattern variables in $x$ by the
corresponding subexpressions of $y$ is a S-expression that is equal to $y$.
And of course if we can't then we wish to be told. Another way to describe the
problem is to specify the behaviour of certain programs, in this case
/sublis/ and /match/, that we wish to write.

{\bf The programs /sublis/ and /match/}

/sublis/ is a program that takes as its input an  S-expression $x$ and an alist $\alpha$
and returns the S-expression $z$ that results by replacing all occurrences of
pattern variables in $x$ by the value associated to them in the alist $\alpha$. Making
the convention that if $\rho$ is a pattern variable and /assoc/[$\rho,\alpha$] is |NIL|
then we make no replacement. 

/match/ is a program that takes as its input two S-expressions $x$,$y$, and an alist$\alpha$.
Given such an input it then returns either an extension of the alist $\alpha↓0$ or the atom
|NO|. In the former case the alist $\alpha↓0$ tells us what values to substitute for the
pattern variables in $x$ to obtain an S-expression equal to $y$. If none can be found,
which is quite often the case then /match/ should return |NO|.

The following are our solutions to these programing problems. We are using
the abstract syntax /isvar/ to avoid unecessary implementaion details detracting
from the simplicity of the algorithms. For the time being the only things 
that we shall assume about /isvar/ is that $/isvar/[\qNIL]=\qNIL$ and
that $/isvar/[x]= \qT \supset /at/[x] = \qT$.
%
\begindefun
(defun sublis (p a)
  (if (atom p)
      (if (isvar p) 
          (let ((w (assoc p a)))  (if (null w) p (cdr w)))
          p)
      (cons (sublis (car p) a) (sublis (cdr p) a))))

\enddefun
%
\begindefun
(defun match (p e a) 
  (if (eq a 'NO)
      'no
      (if (atom p)
          (if (isvar p)
              (let ((w (assoc p a))) (if (null w)
                                         (cons (cons p e) a)
                                         (if (equal (cdr w) e)
                                             a
                                             'no)))
              (if (eq p e) a 'no))
          (if (atom e)
              'no
              (match (cdr p)
                     (cdr e)
                     (match (car p) (car e) a)))
\enddefun
{\bf Some simple properties of /match/}

 In this and subsequent sections it will be helpful if we make a few conventions 
regarding patterns, substitutions and alists. Since we will not be considering
arbitrary alists (as the second argument to /sublis/ and the goal of /match/)
but only those alists all of whose elements have the property that their car 
satisfies /isvar/. We shall call such alists substitution alists, and write
$\alpha \in \qAl{subst}$ to abbreviate this fact.
In the following sections we shall let 
$\rho,\ \rho↓0,\ \rho↓1,\ \ldots$ range over pattern variables.
Given $\alpha↓0,\alpha↓1 \in \qAl{subst}$ we say that $\alpha↓0 \sqsubseteq \alpha↓1$ if we have that
$$\forall \rho\ ((/assoc/[\rho,\ \alpha↓0] \not=\qNIL) \supset
(/assoc/[\rho,\ \alpha↓0]=
/assoc/[\rho,\ \alpha↓1]))$$
Using this notation we have the following basic facts about /match/. The first
proposition expresses the fact that /match/ always terminates.

\noindent{\bf Proposition 1:} If $\alpha \in \qAl{subst}$ then 
$$\forall x,y\ (/match/[x,\ y,\ \alpha] = |NO|) \lor (/match/[x,\ y,\ \alpha] \in \qAl{subst})$$

Notice that we can express some of the content of proposition 1 by the function
mapping equation
$$/match/\ : \qS!\times\qS!\times(\qAl{subst} \cup \{ |NO|\}) \to \qAl{subst} \cup
\{ |NO|\}$$
\noindent{\bf Proof of proposition 1:}\ Is by induction on $r↓{sexp}(x)$,the induction
formula being
$$\Phi[x] = \forall \alpha \in \qAl{subst}\ 
\forall y\ (/match/[x,\ y,\ \alpha] = |NO|) \lor (/match/[x,\ y,\ \alpha] \in \qAl{subst})$$

\noindent{\bf Base case:} Suppose that $x$ is an atom and $y$,$\alpha \in \qAl{subst}$ are such
that $/match/[x,\ y,\ \alpha] \not= |NO|$
then we have to possibilities.

\noindent i.\ $\neg/isvar/[x]$

\noindent In this case we must have that $x=y$ since $/match/[x,\ y,\ \alpha] \not= |NO|$.
Thus 
$$/match/[x,\ y,\ \alpha] = \alpha$$
 and by assumption $\alpha \in \qAl{subst}$.

\noindent ii.\ $/isvar/[x]$

\noindent In this case we have two possibilities, either
$/assoc/[x,\ \alpha] = \qNIL$
$/assoc/[x,\ \alpha] \not= \qNIL$

In the first case we have that 
$$/match/[x,\ y,\ \alpha] = [x \qcons y] \qcons \alpha$$
and since $/isvar/[x] \land \alpha \in \qAl{subst}$ we have $[x \qcons y] \qcons \alpha \in \qAl{subst}$.

In the second case, since $/match/[x,\ y,\ \alpha] \not= |NO|$, we must have that
$/assoc/[x,\ y,\ \alpha] = x \qcons y$ and that $/match/[x,\ y,\ \alpha] = \alpha$ in which case
we certainly have $\alpha \in \qAl{subst}$.

$\qed↓{\bf base\ case}$


{\bf Induction step:} Suppose that $x \in \qC!$ and that $\Phi$ holds for all
s-expressions of less rank than $x$. Furthermore assume that $\alpha \in \qAl{subst}$ and
$/match/[x,\ y,\ \alpha] \not= |NO|$.Then

\noindent$/match/[x,\ y,\ \alpha]$

\noindent$=/match/[\qd x,\qd y,/match/[\qa x, \qa y,\ \alpha]$

\noindent letting $\alpha↓a =/match/[\qa x, \qa y,\ \alpha]$ we have by induction that $\alpha↓a = |NO| \lor
\alpha↓a \in \qAl{subst}$, but since $/match/[x,\ y,\ \alpha] \not= |NO|$ 
we must have $\alpha↓a \in \qAl{subst}$.
Thus

\noindent $=/match/[\qd x,\ \qd y,\ \alpha↓a]$

letting $\alpha↓d =/match/[\qd x,\ \qd y,\ \alpha↓a]$ we have
,again by the induction hypothesis, that $\alpha↓d = |NO| \lor \alpha↓d \in \qAl{subst}$. But
$/match/[x,\ y,\ \alpha] = \alpha↓d$ and so we are done.
$\qed↓{\bf proposition\ 1}$
The next proposition shows that /match/ is in some sense an /increasing/
function.

\noindent{\bf Proposition 2:} If $x\in \qC!$ and $\alpha \in \qAl{subst}$, 
and 
$/match/[x,\ y,\ \alpha] \not= |NO|$, then
$$(/match/[\qa x,\ \qa y,\ \alpha] \sqsubseteq /match/[x,\ y,\ \alpha]) \land
(/match/[\qd x,\ \qd y,\ \alpha] \sqsubseteq /match/[x,\ y,\ \alpha])$$

\noindent{\bf proof of proposition 2:} To prove this we first prove
the following lemma,

\noindent{\bf Lemma:} If $\alpha↓0,\alpha↓1 \in \qAl{subst}$ are  such that

\noindent 1. $/match/[x,\ y,\ \alpha↓1] \not= |NO|$
and 
2. $\alpha↓0 \sqsubseteq \alpha↓1$
then
$$/match/[x,\ y,\ \alpha↓0]\not=|NO|$$
and
$$\alpha↓0 \sqsubseteq /match/[x,\ y,\ \alpha↓0] \sqsubseteq  /match/[x,\ y,\ \alpha↓1]$$

\noindent{\bf Proof of lemma:} is a simple induction on the rank of $x$ and we leave it as
an exercise for the student.

\noindent Now to prove the proposition notice that $/match/[x,\ y,\ \alpha] \not= |no|$ thus

\noindent $/match/[x,\ y,\ \alpha]$

\noindent $=/match/[\qd x,\ \qd y,\ /match/[\qa x,\ \qa y,\ \alpha]]$

\noindent now by the lemma $\alpha↓a = /match/[\qa x,\ \qa y,\ \alpha] \sqsupseteq \alpha$, thus

\noindent $=/match/[\qd x,\ \qd y,\ \alpha↓a]$

\noindent Thus since $\alpha \sqsubseteq \alpha↓a$ we have that
$$/match/[\qa x, \qa y, \ \alpha] \sqsubseteq /match/[x,\ y,\ \alpha]$$
and
$$/match/[\qd x, \qd y, \ \alpha] \sqsubseteq /match/[x,\ y,\ \alpha]$$
$\qed↓{\bf proposition 2}$
The next result shows that $/match/[x,\ y,\ \alpha]$ and any extension of it
is a solution for $\beta$ in the equation:
$$/match/[x,\ y,\ \beta] = \beta$$

\noindent{\bf Proposition 3: }
Suppose that $\alpha↓0,\ \alpha↓1 \in \qAl{subst}$ are such 
that 

1.\ $/match/[x,\ y,\ \alpha↓0] \not=|NO|$,
and
2.\ $/match/[x,\ y,\ \alpha↓0] \sqsubseteq \alpha↓1$ 

\noindent Then
$$/match/[x,\ y,\ \alpha↓1] = \alpha↓1$$

\noindent{\bf proof of proposition 3:}\ Is by induction on $r↓{sexp}(x)$ with induction
formula $\Phi[x]$ being
$\forall \alpha↓0,\alpha↓1 \in \qAl{subst},\ \forall y\  \Psi$ where $\Psi$ is
$$(/match/[x,\ y,\ \alpha↓0] \not= |NO|) \land
(/match/[x,\ y,\ \alpha↓0] \sqsubseteq \alpha↓1) \supset
(/match/[x,\ y,\ \alpha↓1] = \alpha↓1)$$

\noindent Assume in what follows that
$\alpha↓0,\ \alpha↓1$ and
$y$ are such that
$$(/match/[x,\ y,\ \alpha↓0] \not= |NO|) \land
(/match/[x,\ y,\ \alpha↓0] \sqsubseteq \alpha↓1)$$
\noindent then

\noindent{\bf Base case:} Assume that $x$ is an atom, in otherwords $r(x)=0$
then we have two cases.

\noindent i. $\neg/isvar/[x]$

\noindent In this case we must have that $x = y$ and consequently we have
$$\forall \alpha \in \qAl{subst}\ /match/[x,\ y,\ \alpha] = \alpha$$
so in particular
$$/match/[x,\ y,\ \alpha↓1] = \alpha↓1$$

\noindent ii. $/isvar/[x]$

\noindent In this case we have two possibilities either 
$/assoc/[x,\ \alpha↓0] = \qNIL$ or $/assoc/[x,\ \alpha↓0] \not= \qNIL$.

\noindent In the first case 
$$/match/[x,\ y,\ \alpha↓0] = [x \qcons y] \qcons \alpha↓0$$
and since
$$/match/[x,\ y,\ \alpha↓0] \sqsubseteq \alpha↓1$$
we have  that $/assoc/[x,\ \alpha↓1] = x \qcons y$, consequently
$$/match/[x,\ y,\ \alpha↓1] = \alpha↓1$$.

\noindent In the second case we have that
$/assoc/[x,\ \alpha↓0] = x \qcons y$ and $/match/[x,\ y,\ \alpha↓0] = \alpha↓0$
, consequently
$/assoc/[x,\ \alpha↓1] = x \qcons y$ since
$$/match/[x,\ y,\ \alpha↓0] \sqsubseteq \alpha↓1.$$
Thus
$$/match/[x,\ y,\ \alpha↓1] = \alpha↓1.$$
$\qed↓{\bf base\ case}$

\noindent{\bf Induction step:} Now assume that $x \in \qC!$ and that $\Phi$
holds for all s-expressions of less rank that $x$. Since 
$/match/[x,\ y,\ \alpha↓0] \not= NO$ we must have that $y \in \qC!$ as well.
Thus

\noindent$/match/[x,\ y,\ \alpha↓1]$

\noindent$=/match/[\qd x,\ \qd y,\ /match/[\qa x,\ \qa y,\ \alpha↓1]]$

but by proposition 2 $\alpha↓1 \sqsupseteq /match/[\qa x,\ \qa y,\ \alpha↓0]$ so
the induction hypothesis  allows us to conclude
that $/match/[\qa x,\ \qa y, \alpha↓1] = \alpha↓1$ thus

\noindent$=/match/[\qd x,\ \qd y,\ \alpha↓1]$

which again by proposition 2 and the induction hypothesis becomes

\noindent$=\alpha↓1$

$\qed↓{\bf proposition\ 3}$
\noindent{\bf Correctness of /match/}

The main result we prove in this section is the following result that
demonstrates that /match/ does indeed do what we want it to, at least
when it succeeds.

{\bf Theorem 1:} If $\alpha \in \qAl{subst}$ is such that
\noindent$/match/[x,\ y,\ \alpha] \not= |NO|$ then
$$/sublis/[x,\ /match/[x,\ y,\ \alpha]] = y$$

\noindent{\bf Proof of Theorem:} The proof is by rank induction on $x$, with the usual
definition of s-expression rank and induction formula:
$$\Phi[x] = \forall y\ \forall \alpha \in \qAl{subst}\ 
(/match/[x,\ y,\ \alpha] \not= |NO|) \supset 
/sublis/[x,\ /match/[x,\ y,\ \alpha]] = e$$

\noindent{\bf Base case:} $r↓{sexp}(x)=0$. In this case we have that $x$ is an atom.
Suppose that $/match/[x,\ y,\ \alpha] \not= |NO|$ then 
we have two cases.

\noindent i. $\neg /isvar/[x]$.

\noindent Since $/match/[x,\ y,\ \alpha] \not= |NO|$ we must have
that $x = y$ consequently
$$y = x = /sublis/[x,\ y, \alpha]$$

\noindent ii.$/isvar/[x]$.

\noindent In this case we have two possibilities, either
$/assoc/[x,\ \alpha] = \qNIL$ or $/assoc/[x,\ \alpha] \not= \qNIL$.
If $/assoc/[x,\ \alpha] = \qNIL$ then since
$/match/[x,\ y,\ \alpha] \not= |NO|$
we must have that 
$$/match/[x,\ y,\ \alpha] = [x \qcons y] \qcons \alpha.$$
 In which case
$$/sublis/[x,\ [x \qcons y] \qcons \alpha] = \qd[x \qcons y] = y$$
So suppose that:
$/assoc/[x,\ \alpha] \not= \qNIL$
then again since
$/match/[x,\ y,\ \alpha] \not= |NO|$ we must have that $/assoc/[x,\ \alpha] = x \qcons y$.
Thus $/sublis/[x,\ \alpha] = y$.

$\qed↓{\bf base\ case}$

\noindent{\bf Induction step:} Suppope that $x \in \qC!$ and that $\Phi$ holds for all
s-expressions of less rank than $x$. Furthermore suppose that
$/match/[x,\ y,\ \alpha] \not= |NO|$, then clearly $y \in \qC!$ as well.

\noindent{\bf Lemma:} Under these circumstances we have the following.

1. $/match/[x,\ y,\  /match/[x,\ y,\ \alpha]] = /match/[x,\ y,\ \alpha]$

2. $/match/[\qa x,\ \qa y,\  /match/[x,\ y,\ \alpha]] = /match/[x,\ y,\ \alpha]$

3. $/match/[\qd x,\ \qd y,\  /match/[x,\ y,\ \alpha]] = /match/[x,\ y,\ \alpha]$


\noindent The proof of which is a simple corollary to propositions 2 and 3.
Now using the definition of /sublis/ we have

\noindent $/sublis/[x,\ /match/[x,\ y,\ \alpha]]$


\noindent $= /sublis/[\qa x,\ /match/[x,\ y,\ \alpha]] \qcons
/sublis/[\qd x,\ /match/[x,\ y,\ \alpha]]$

\noindent which letting $\alpha↓1 = /match/[x,\ y,\ \alpha]$ becomes, using the lemma

\noindent $= /sublis/[\qa x,\ /match/[x,\ y,\ \alpha↓1]] \qcons
/sublis/[\qd x,\ /match/[x,\ y,\ \alpha↓1]]$

\noindent again by the lemma we have that this is 

\noindent $= /sublis/[\qa x,\ /match/[\qa x,\ \qa y,\ \alpha↓1]] \qcons
/sublis/[\qd x,\ /match/[\qd x,\ \qd y,\ \alpha↓1]]$

\noindent Now by the induction hypothesis we have that this

\noindent $=\qa y \qcons \qd y$

\noindent $=y$.

$\qed↓{\bf theorem\ 1}$
So far we have proved that if /match/ is successful then it does what we want it to
do. But what happens when it fails? To really be sure of the correctness of our
program we would also like to be able to show that if /match/ fails then there was
a good reason for it to fail. The following theorem expresses this fact. We will
not prove this theorem here, rather it will turn out to be a corollary of a more
general theorem that we shall prove in the next section. 

\noindent{\bf Theorem 2:} If $\alpha \in \qAl{subst}$ and $/match/[x,\ y,\ \alpha]=|NO|$ then
$$\forall \alpha↓0 \in \qAl{subst}\ ((\alpha \sqsubseteq \alpha↓0) \supset (/sublis/[x,\ \alpha↓0]\not= y))$$


So although our program /match/ does what we want it to do, it does not do all
that one could possibly ask of it. It assumes that the expression it is
attempting to match with the pattern does not contain any pattern variables.
At least in the sense that it does not make use of this fact. Consider the
following example

/pattern/ $= (\rho\ \rho )$

/expression/ $= ( \rho\ |A| )$

\noindent in this example $/match/[pattern,\ expression,\ \qNIL] = |NO|$
even though in some sense there is a match to be found. In the next section
we shall deal with this more general problem of trying to match two patterns.
This problem is traditionally known as unification and is used extremely
frequently in mechanical proof checkers and theorem provers. It being
origonally introduced by Robinson in connection to the resolution method
of proof checking.

The following are simple properties of /sublis/, /occur/ and /compose/
that are left as exercises, some of them will be used in the next section.
In these exercises and the following section we shall use the following
abbreviations:

$\rho \in dom(\alpha) \liff \neg\qn/assoc/[\rho, \alpha]$

If $\rho \in dom(\alpha)$ then $\alpha(\rho)=\qd /assoc/[\rho, \alpha]$

$\alpha\circ\beta = /compose/[\alpha, \beta]$

where the programs /occur/ and /compose/ are defined by:
\begindefun
(defun occur (x y)
  (if (atom y)
      (eq x y)
      (or (occur x (car y))
          (occur x (cdr y))) ) )
(defun compose (a b) (append (subsub a b) b))
(defun subsub (a b) (if (null a) a (cons (cons (caar a) (sublis (cdar a) b))
                                         (subsub (cdr a) b))))
\enddefun

\exercise If $\forall\rho↓1\in dom(\alpha)\ \neg/occur/[\rho↓0,\alpha(\rho↓1)]$
and $\rho↓0 \in dom(\alpha)$ 

then $\neg/occur/[\rho↓0, /sublis/[x \alpha]]$

\exercise $/sublis/[x, \alpha] = /sublis/[x, \alpha\downarrow↓x]$ 

where $\alpha\downarrow↓x\sqsubseteq \alpha$ is the restriction of $\alpha$ to
$dom(\alpha) \cap \{ \rho \mid /occur/[\rho, x] \}$

\exercise $/sublis/[x, \qNIL] = x$

\exercise If $\alpha \sqsubseteq \beta$ and $/sublis/[x, \alpha] = /sublis/[y, \alpha]$
then 
$/sublis/[x, \beta] = /sublis/[y, \beta]$

\exercise $/sublis/[x , \alpha\circ\beta] =/sublis/[/sublis/[x, \alpha], \beta]$

\exercise $/sublis/[x, \alpha\circ(\beta\circ\gamma)]=
/sublis/[x, (\alpha\circ\beta)\circ\gamma]$


\section{Unification}
\sectlab{Unifi}

In this section we will study the problem of determining whether two patterns
have a common instance. Suppose that $x↓1$ and $x↓2$ are patterns, we say that
an $A \in \qAl{subst}$ unifies $x↓1$ and $x↓2$ if the result of carrying out the
substitutions given by $A$ in $x↓1$ is equal to the result of carrying out the same
substitutions in $x↓2$.

We shall specify a program /unify/ such that if $/unify/[x↓1,\ x↓2] \not= |NO|$
then 
$$/sublis/[x↓1,\ /unify/[x↓1,\ x↓2]] =
/sublis/[x↓2,\ /unify/[x↓1,\ x↓2]]$$

\begindefun
(defun unify (x y) (uni x y 'nil))
(defun uni (x y a)
  (cond ((or (eq a 'no) (eq x y)) a)
        ((isvar x) (if (occur x y) 'no (compose a (cons (cons x y) nil))))
        ((isvar y) (if (occur y x) 'no (compose a (cons (cons y x) nil))))
        ((or (atom x) (atom y)) 'no)
        ( T (let ((b (uni (car x) (car y) a)))
              (if (eq b 'no)
                  'no
                  (uni (sublis (cdr x) b)
                       (sublis (cdr y) b)
                       b) ) ) ) ) )
\enddefun
The algorithm this program implements is called the {\it left-first mesh
substitution}. It does a /left-first/ search for a point of dissagreement
between $x$ and $y$. If it fails to find one then of course $x$ and $y$ are
already equal. So pressuming that it discovers a point of dissagreement
between $x$ and $y$ it then checks to see if this dissgreement is
removable by assigning a value to a pettern variable, if so it extends the alist
appropriately. Then before backtraking and proceeding with the rest of $x$ and $y$
it makes the forced substitutions. If it cannot rectify the dissagreement it
immediately returns |NO|.

There is one well known subtle point concerning /unification/. If a pattern variable
is forced to be matched against a non-atomic s-expression that itself contains
the pattern variable. Then unless one is allowed destructive substitutions that
will create re-entrant s-expressions, no unification is possible . This gives
rise to the so-called /occurence/ /check/. There is one point concerning our
program which may not be immediately obvious. Once a pattern variable
is assigned a value it should never be encountered again. This is because we 
do an occurence check and then actually replace the pattern variable by its
associated value.
\noindent{\bf Theorem 3:}
$\forall x,y\ (/unify/[x,\ y] = |NO|) \lor (/unify/[x,\ y] \in \qAl{subst})$

We actually prove theorem 3 by proving a much stronger  but somewhat
more tedious result, namely.

\noindent{\bf Termination lemma:}
If $\alpha \in \qAl{subst}$ is such that

\noindent 1.\ $\forall \rho \in dom(\alpha )\ \neg/occur/[\rho,\ x\qcons y]$
 and 
2.$\forall \rho↓0,\ \rho↓1 \in dom(\alpha )\ \neg /occur/[\rho↓0,\ \alpha (\rho↓1)]$

\noindent then either
$$/uni/[x,\ y,\ \alpha] = |NO| \lor /uni/[x,\ y,\ \alpha] = \beta$$
\noindent where $\beta$ has the following properties

\noindent P1. $\exists \gamma\ ( (dom(\alpha) \cap dom(\gamma) = \emptyset) \land (\beta
= \alpha \circ \gamma))$

\noindent P2. $\forall \rho↓0,\ \rho↓1 \in dom(\beta)\ \neg/occur/[\rho↓0,\ \beta(\rho↓1)]$

\noindent P3. $\forall \rho↓0,\ \rho↓1 \in dom(\gamma)\ ( (/occur/[\rho↓0,\ x\qcons y]) \land
(/occur/[\rho↓1,\ \gamma[\rho↓0] \supset /occur/[\rho↓1,\ x\qcons y]) )$

\noindent{\bf Proof of lemma:}  
Rather than do the following proofs by rank induction we take this opportunity
to give some examples of proofs by induction on well-founded relations.
This proof is induction on the wellfounded ralation
$\prec↓u$ which is defined by


$x↓1\qcons y↓1 \prec↓u x↓2 \qcons y↓2$

iff either

i. $r↓{var}(x↓1\qcons y↓1) < r↓{var}(x↓2 \qcons y↓2)$

or 

ii. $r↓{var}(x↓1\qcons y↓1) = r↓{var}(x↓2 \qcons y↓2)$ and
$r↓{sexp}(x↓1).r↓{sexp}(y↓1) < r↓{sexp}(x↓2).r↓{sexp}(y↓2)$

\noindent where $r↓{var}(x)$ is the number of distinct pattern variables that
occur in $x$.

Thus the following proofs will be almost identical in form to those that would
be obtained if we did induction on $r↓{u}(x\qcons y)$ where:

$$r↓{u}(x\qcons y) = r↓{var}(x\qcons y).\omega + r↓{sexp}(x).r↓{sexp}(y)$$

\noindent{\bf Base case:} Suppose that $x \qcons y$ is $\prec↓u$ minimal, in
otherwords no pattern variables occur in either $x$ or $y$ and at least one is
atomic. In this case we have that either $x=y$ or $x \not=y$. If $x =y$ then
$$/uni/[x,\ y,\ \alpha] = \alpha$$
and letting $\gamma = \qNIL$ gives the result. On the other hand if $x \not=y$
then
$$/uni/[x,\ y,\ \alpha] = |NO|$$
$\qed↓{\bf base\ case}$

\noindent{\bf Induction step:} Suppose that $x\qcons y$ is not $\prec↓u$ minimal
and that the lemma holds for $x↓0\qcons y↓0 \prec↓u  x\qcons y$. Without loss
of generality we may assume that $x \not=y$ and either

\noindent 1. $/isvar/[x]$

\noindent 2. $\neg/isvar/[x] \land /isvar/[y]$

\noindent or

\noindent 3. $x,\ y \in \qC!$.

Since if $x = y$ then
$$/uni/[x,\ y,\ \alpha] = \alpha$$
while if $x \not= y$ and none of 1,2 or 3 held then
$$/uni/[x,\ y,\ \alpha] = |NO|.$$

\noindent{\bf case 1:} In this case we have two possibilities, either $/occur/[x,\ y]$
in which case $/uni/[x,\ y,\ \alpha] = |NO|$ or $\neg/occur/[x,\ y]$. So suppose
that $\neg/occur/[x,\ y]$ then letting $\gamma = < x\qcons y>$ we have
$$/uni/[x,\ y,\ \alpha] = \alpha\circ\gamma = \beta.$$
Now by assumption on $\alpha$ we have
$(dom(\alpha) \cap dom(\gamma) = \emptyset)$ so P1 of the lemma holds. P3 is trivially
true, so all that remains is to show that P2 holds in this case.
To prove that  $\forall \rho↓0,\ \rho↓1 \in dom(\beta)\ \neg/occur/[\rho↓0,\ \beta(\rho↓1)]$
it suffices to observe that

\noindent i. $\rho↓0 \in dom(\alpha)\ \supset\ \neg/occur/[\rho↓0,\ y]$

\noindent ii. $\neg/occur/[x,\ y]$, and

\noindent iii.$\neg/occur/[x,\ \alpha\circ\gamma(\rho↓0)]\ ,\ \rho↓0 \in dom(\alpha)$.

Of these i. and ii. are immediate while iii. follows from the fact that
$$\alpha\circ\gamma(\rho↓0) = /sublis/[\alpha(\rho↓0),\ <x\qcons y>]$$
and since $\neg/occur/[x,\ y]$ we must have that
$$\neg/occur/[x,\ /sublis/[\alpha(\rho↓0),\ <x\qcons y>]]$$.
$\qed↓{\bf case\ 1}$

\noindent{\bf case 2:} Is almost identical to case one so we leave the details for the
student to verify.
$\qed↓{\bf case\ 2}$

\noindent{\bf case 3:} $x,\ y \in \qC!$. In this case since
$$\qa x \qcons \qa y\ \prec↓u x \qcons y$$
we have by induction hypothesis that either
$$/uni/[\qa x,\ \qa y,\ \alpha]= |NO| \lor /uni/[\qa x,\ \qa y,\ \alpha]= \beta↓a$$
and $\beta↓a = \alpha\circ\gamma↓a$ satisfies P1,P2 and P3.

If $/uni/[\qa x,\ \qa y,\ \alpha]=|NO|$ then $/uni/[x,\ y, \alpha]=|NO|$ and we are done.
So suppose to the contrary that
$$/uni/[\qa x,\ \qa y,\ \alpha]= \beta↓a$$
then we make the claim 

\noindent{\bf Claim:} 
$x↓d\qcons y↓d =/sublis/[\qd x,\ \beta↓a]\qcons /sublis/[\qd y,\ \beta↓a] \prec↓u x\qcons y$
	
\noindent{\bf proof of claim:} We have two cases, if $\beta↓a = \alpha$ then trivially
$x↓d\qcons y↓d = \qd x\qcons \qd y \prec↓u x \qcons y$ so suppose that $\rho↓0 \in
dom(\gamma↓a)$, then since $\neg/occur/[\rho↓0,\ \beta↓a(\rho↓1)]$ we must have that
$$\neg/occur/[\rho↓0,\ /sublis/[\qd x,\ \beta↓a]]$$
and
$$\neg/occur/[\rho↓0,\ /sublis/[\qd y,\ \beta↓a]]$$
thus $r↓{var}(x↓d\qcons\ y↓d) < r↓{var}(x \qcons y)$
$\qed↓{\bf claim}$

So by the induction hypothesis
$$/uni/[ x↓d,\ y↓d,\ \beta↓a]= |NO| \lor /uni/[x↓d,\ y↓d,\ \beta↓a]= \beta↓d$$
and $\beta↓d = \alpha\circ\gamma↓d$ satisfies P1,P2 and P3. Again we may assume
that $/uni/[x↓d,\ y↓d,\ \beta↓a] \not= |NO|$,thus
$$/uni/[ x,\ y,\ \alpha]= \beta = /uni/[x↓d,\ y↓d,\ \beta↓a]= \beta↓d$$
Clearly since $\beta↓d$ has property P2 we also have that $\beta$ has property
P2. To verify P1 notice that
$$/uni/[x,y,\alpha]=(\alpha\circ\gamma↓a)\circ\gamma↓d=\alpha\circ(\gamma↓a\circ
\gamma↓d)=\alpha\circ\gamma$$
and by virtue of $\gamma↓a$ and $\gamma↓d$ we have that
$$dom(\alpha) \cap dom(\gamma) = \emptyset$$ 
Thus all that remains is to verify P3. If $\rho\in dom(\gamma)$ then either
$\rho\in dom(\gamma↓a)$ or $\rho\in dom(\gamma↓d)$. In the former case we
know by induction that $/occur/[\rho,\ \qa x\qcons \qa y]$ so suppose that
the later holds. Then by induction $/occur/[\rho, x↓d\qcons y↓d]$ which
implies that either $/occur/[\rho, \qd x \qcons \qd y] \lor
/occur/[\rho, \gamma↓a(\rho↓0)]$ for some $\rho↓0 \in dom(\gamma↓a)$. In any
case we can conclude that $/occur/[\rho,\ x\qcons y]$. The second part of
P3 we leave as an exercise.

$\qed↓{\bf termination\ lemma}$

$\qed↓{\bf Theorem\ 3}$
The fact that /unify/, when it succeeds, does what we want it to do 
is expressed by the  following result.

\noindent{\bf Theorem 4:} If $/unify/[x,\ y] \not= |NO|$ then
$/sublis/[x,\ /unify/[x,\ y]] =
/sublis/[y,\ /unify/[x,\ y]]$

\noindent{\bf Proof:} We prove by induction on $\prec↓u$ that if $\alpha$
satisfies the hypothesis of the termination lemma and  if 
$/uni/[x,\ y,\ \alpha]=\beta\not=|NO|$ then we must have that
$$/sublis/[x,\ \beta]=/sublis/[y,\ \beta].$$

\noindent{\bf Base case:} If $x\qcons y$ is $\prec↓u$ minimal then neither
$x$ nor $y$ can contain any pattern variables and at least one is atomic.
Furthermore since $/uni/[x,\ y,\ \alpha]$ is assumed to be different from
|NO| we must have that $x=y$. Since $/uni/[x,\ y,\ \alpha]=\alpha$ we conclude
$$/sublis/[x,\alpha]=x=y=/sublis/[y,\alpha]$$
$\qed↓{\bf base\ case}$


\noindent{\bf Induction step:} Assume that $x\qcons y$ is not $\prec↓u$ minimal
and that the result holds for all $x↓1\qcons y↓1 \prec↓u x\qcons y$. As in the 
proof of the termination lemma we may assume that $x\not=y$ and either

\noindent 1. $/isvar/[x]$

\noindent 2. $\neg/isvar/[x] \land /isvar/[y]$

\noindent or

\noindent 3. $x,\ y \in \qC!$,

\noindent And that $/uni/[x,\ y,\ \alpha]\not=|NO|$.

\noindent{\bf Case 1:} If $x$ is a pattern variable then since
$/uni/[x,\ y,\ \alpha]\not=|NO|$ we must have that $\neg/occur/[x,y]$ and
$/uni/[x,\ y,\ \alpha]= \alpha\circ <x \qcons y>= \beta$

Now under these circumstances $/sublis/[x, \beta] = y$ and 
$/sublis/[y, \beta] = y$ by assumption on $\alpha$ and the fact that
$\neg/occur/[x, y]$.
$\qed↓{\bf case\ 1}$

\noindent{\bf Case 2:} Again is simply a slight variation on case 1 and we ommit
it to avoid repitition.
$\qed↓{\bf case\ 2}$

\noindent{\bf Case 3:} $x,y \in \qC!$. In this case let
$$\beta↓a =/uni/[\qa x,\ \qa y,\ \alpha]$$
So since $\beta↓a\not=|NO|$ and by induction
$$/sublis/[\qa x, \beta↓a]=/sublis/[\qa y, \beta↓a]$$

Now as in the proof of the termination lemma we have that 
$$x↓d\qcons y↓d =/sublis/[\qd x,\ \beta↓a]\qcons /sublis/[\qd y,\ \beta↓a] \prec↓u x\qcons y$$

So again by induction we have $/uni/[x↓d,\ y↓d,\ \beta↓a]=\beta=\beta↓a\circ\gamma↓d$
and 
$$/sublis/[\qa x, \beta↓a]=/sublis/[\qa y, \beta↓a]$$
Now 
\noindent$/sublis/[x↓d,\ \beta]$

\noindent$=/sublis/[x↓d,\ \gamma↓d]$

\noindent since $\rho \in dom(\beta↓a) \supset \neg/occur/[\rho,\ x↓d]$

\noindent$=/sublis/[/sublis/[\qd x,\ \beta↓a] \gamma↓d]$

\noindent$=/sublis/[\qd x,\ (\beta↓a\circ\gamma↓d)]$

\noindent$=/sublis/[\qd x,\ \beta]$

Also by symetry we have that 
$$/sublis/[y↓d,\ \beta]=/sublis/[\qd y,\ \beta].$$
So
Furthermore since
$$/sublis/[\qa x,\ \beta↓a]=/sublis/[\qa y,\ \beta↓a]$$
we have
$$/sublis/[/sublis/[\qa x,\ \beta↓a],\ \gamma↓d]=/sublis/[/sublis/[\qa y,\ \beta↓a],\ \gamma↓d]$$
or in otherwords
$$/sublis/[\qa x,\ \beta]=/sublis/[\qa y,\ \beta]$$
Consequently
$$/sublis/[ x,\ \beta]=/sublis/[ y,\ \beta]$$
$\qed↓{\bf theorem\ 4}$

The fact that /unify/ does indeed succeed whenever it can is the task of the next
two results.
Firstly we prove that our unification program actually finds a {\it most general
unification}. By this we mean that any other unification can be obtained
from the one our program returns by a further composition.

\noindent{\bf Theorem 5:} If $\gamma$ unifies $x$ and $y$ then
$/unify/[x,\ y,]=\beta \in \qAl{subst}$ and
$$\exists \delta \in \qAl{subst}\ \forall z /sublis/[z,\ \gamma]=/sublis/[z,\ \beta\circ\delta]$$

We shall write $\delta↓0\equiv \delta↓1$ to abbreviate the fact that
$\forall z /sublis/[z,\ \delta↓0]=/sublis/[z,\ \delta↓1]$.

\noindent{\bf Proof of theorem:} We prove by induction on the relation
$\prec↓u$ that if $\alpha$ satisfies the hypothesis of the termination
lemma and if $\gamma$ unifies $x$ and $y$ as well as there existing a
$\delta↓0 \in \qAl{subst}\ \gamma \equiv \alpha\circ\delta↓0$ then
$$(/uni/[x,\ y,\ \alpha] = \beta \in \qAl{subst}) \land (\exists \delta\in \qAl{subst}\ 
\gamma \equiv \beta\circ\gamma)$$

\noindent{\bf Base case:} If $x\qcons y$ is $\prec↓u$ minimal then as usual
neither $x$ nor $y$ contain any pattern varables, consequently since they are
unifiable they must be equal. Thus $/uni/[x,\ y,\ \alpha]=\alpha$ and our
initial assumption concerning $\alpha$ gives the result.
$\qed↓{\bf base\ case}$

\noindent{\bf Induction step:} As per usual we may assume that $x\not=y$
and that either

\noindent 1. $/isvar/[x]$

\noindent 2. $\neg/isvar/[x] \land /isvar/[y]$

\noindent or

\noindent 3. $x,\ y \in \qC!$.

\noindent{\bf Case 1:} In this situation we have two possibilties, namely
i.\ $\neg/isvar/[y]$ or ii.\ $/isvar/[y]$.

\noindent i.\ In this case since $x$ and $y$ are unifiable we cannot have
that $/occur/[x,y]$ (otherwise since $x\not=y$ we must have that $y\in \qC!$
and then an easy induction would show that 
$r↓{sexp}(/sublis/[x,\gamma])< r↓{sexp}(/sublis/[y,\gamma])$ contradicting supposed
equality.)
Thus $/uni/[x,y,\alpha] = \alpha\circ<x\qcons y>$ . Also since $\gamma$ unifies
$x$ and $y$ and $x \not\in dom(\alpha)$ we have that
$$\delta↓0(x)=\gamma(x)= /sublis/[y, \gamma] =/sublis/[y,\delta↓0]$$
the last equality holding because no pattern variable that occurs in $dom(\alpha)$
occurs in $y$.
Using the following simple lemma 

\noindent{\bf Lemma:} If $\alpha,\delta \in \qAl{subst}$ and $x$ and $y$ are such
that $x \in dom(\delta)$ and $/sublis/[y,\delta]=\delta(x)$
then
$$\alpha\circ\delta\equiv(\alpha\circ<x\qcons y>)\circ\delta$$

\noindent leaving the proof of the lemma aside for a moment, observe that
$$\alpha\circ\delta↓0\equiv(\alpha\circ<x\qcons y>)\circ\delta↓0
=\beta\circ\delta↓0$$
and so the result  holds when $\neg/isvar/[y]$.

\noindent{\bf proof of lemma:}

\noindent$/sublis/[z, (\alpha\circ<x\qcons y>)\circ\delta]
=/sublis/[z,  \alpha\circ(<x\qcons y>\circ\delta)]$

\noindent and and it is an easy  task to show that under the hypothesis
$$<x\qcons y>\circ\delta = <x\qcons /sublis/[y,\delta]>\qapp\delta
= <x\qcons \delta(x)>\qapp\delta \equiv \delta$$
so the lemma follows.
$\qed↓{\bf lemma}$

\noindent ii.\ $/isvar/[y]$,is this situation there are three alternatives
a.\ $(x \in dom(\gamma) \land y \not\in dom(\gamma))$
b.\ $(x \in dom(\gamma) \land y \in dom(\gamma))$
c.\ $(x \not\in dom(\gamma) \land y \in dom(\gamma))$
and by assumption on $\alpha$ we know that n all three cases that
$$/uni/[x,y,\alpha] = \alpha\circ<x\qcons y>$$

\noindent a. In this case we have that $\gamma(x)=y$ and as $x\not\in dom(\alpha)$
we also have that $\delta↓0(x)=y$ thus

$$\gamma \equiv \alpha\circ\delta↓0$$
and by the lemma
$$\alpha\circ\delta↓0 \equiv (\alpha\circ<x\qcons y>)\circ\delta↓0 = \beta\circ\delta↓0$$

\noindent b. In this case we have that 
$$\gamma(x)=\delta↓0(x)=\delta↓0(y)=\gamma(y)$$
and as in the previous case we have
$$\gamma \equiv \alpha\circ\delta↓0$$
and by the lemma
$$\alpha\circ\delta↓0 \equiv (\alpha\circ<x\qcons y>)\circ\delta↓0 = \beta\circ\delta↓0$$

\noindent c. In this case we have that $\gamma(y)=\delta↓0(y) = x$ and $x \not\in
dom(\gamma)$.However clearly $<x\qcons x>\qcons \gamma \equiv \gamma$ and so this case
just reduces to the previous situation.
$\qed↓{\bf case\ 1}$

\noindent{\bf Case 2:} Is exactly the same as case one except that there is one less
alternative, since we know that $\neg/isvar/[x]$. We leave the details for the student to fill
in.
$\qed↓{\bf case\ 2}$


\noindent{\bf case\ 3:} $x,y \in \qC!$. By induction we have that
$$/uni/[x,y,\alpha] = \beta↓a \land \gamma\equiv\beta↓a\circ\delta↓a$$
We claim that $x↓d =/sublis/[\qd x, \beta↓a]$ and $y↓d =/sublis/[\qd y, \beta↓a]$
are unified by $\gamma$ since

\noindent$/sublis/[x↓d,\gamma]$

\noindent$=/sublis/[x↓d,\beta↓a\circ\delta↓a]$

\noindent$=/sublis/[/sublis/[\qd x,\beta↓a],\beta↓a\circ\delta↓a]$

but by the properties of $\beta↓a$ given by the termination lemma we have

\noindent$=/sublis/[/sublis/[\qd x,\beta↓a],\delta↓a]$

\noindent$=/sublis/[\qd x,\beta↓a\circ\delta↓a]$

\noindent$=\qd /sublis/[ x,\gamma]$

\noindent$=\qd /sublis/[ y,\gamma]$

which by the same sequence of steps is

\noindent$=/sublis/[y↓d,\gamma]$

So one more application of the induction hypothesis gives the result.
$\qed↓{\bf Case\ 3}$

$\qed↓{\bf theorem 5}$
As a simple application of the previous theorem we can prove that
/unify/ only fails whenever it cannot do otherwise.

\noindent{\bf Theorem 6:} If $/unify/[x,\ y]=|NO|$ then
$\forall A \in \qAl{subst}\ (/sublis/[x,\ A]\not=/sublis/[y,\ A])$

\noindent{\bf Proof of Theorem:} Again the proof is by induction on
$\prec↓u$  with the hypothesis being that if $\alpha$ satisfies the conditions
of the termination lemma then if $/uni/[x,y,\alpha]=|NO|$ then
$$\forall \beta \in \qAl{subst}\ (/sublis/[x,\ \beta]\not=/sublis/[y,\ \beta])$$
Suppose that $/uni/[x,y,\alpha]=|NO|$ .

\noindent{\bf Base case:} If neither $x$ nor $y$ contain any pattern variables
and they are distinct (as they must be for $/uni/[x,y,\alpha]=|NO|$) then
$$\forall \beta \in \qAl{subst}\ (x=/sublis/[x,\ \beta]\not=/sublis/[y,\ \beta]=y)$$
$\qed↓{\bf base\ case}$

\noindent{\bf Induction step:} As usual we only deal with the situation when
either
(note that by assumption we cannot have $x=y$).

\noindent 1. $/isvar/[x]$

\noindent 2. $\neg/isvar/[x] \land /isvar/[y]$

\noindent or

\noindent 3. $x,\ y \in \qC!$.

Since the result is trivial if neither $x$ nor $y$ is a pattern variable and
at least one is atomic.

\noindent{\bf Case 1:} If $/isvar/[x]$ then we must have that $/occur/[x,y]$
and by exactly the same reasoning as used in the last theorem we must
have that $y\in \qC!$ and $x$ and $y$ are not unifiable. the proof
of case 2 is identical.
$\qed↓{\bf case\ 1\ and\ 2}$

\noindent{\bf Case 3:} $x,y \in \qC!$, if 
$/uni/[\qa x, \qa y, \alpha]=|NO|$ then by induction
$$\forall \beta \in \qAl{subst}\ (/sublis/[\qa x,\ \beta]\not=/sublis/[\qa y,\ \beta])$$
thus by definition of $/sublis/$
$$\forall \beta \in \qAl{subst}\ (\qa /sublis/[x,\ \beta]\not=\qa /sublis/[y,\ \beta])$$
and thus
$$\forall \beta \in \qAl{subst}\ (/sublis/[x,\ \beta]\not=/sublis/[y,\ \beta])$$

So suppose that 
$/uni/[\qa x, \qa y, \alpha]=\gamma↓a\in \qAl{subst}$ then by definition
$/uni/[x↓d, y↓d, \alpha]=|NO|$ where 
$x↓d=/sublis/[\qd x,\gamma↓a]$ and
$y↓d=/sublis/[\qd y,\gamma↓a]$
and by induction
$$\forall \beta \in \qAl{subst}\ (/sublis/[x↓d,\ \beta]\not=/sublis/[y↓d,\ \beta])$$

So suppose that $\beta$ unified $x$ and $y$, then by the previous theorem
and the simple fact that $\beta$ must unify $\qa x$ and $\qa y$ we have
$\beta \equiv \gamma↓a\circ\delta$ for some $\delta\in \qAl{subst}$
but

\noindent$/sublis/[x↓d, \beta]$

\noindent$=/sublis/[/sublis/[\qd x,\gamma↓a],\beta]$

\noindent$=/sublis/[/sublis/[\qd x,\gamma↓a],\gamma↓a\circ\delta]$

\noindent$=/sublis/[/sublis/[\qd x,\gamma↓a],\delta]$

\noindent$=/sublis/[\qd x,\gamma↓a\circ\delta]$

\noindent$=/sublis/[\qd x,\beta]$

\noindent$=/sublis/[\qd y,\beta]$

\noindent$/sublis/[y↓d, \beta]$

which is a contradiction, thus no such $\beta$ exists and we are done.
$\qed↓{\bf theorem\ 6}$
The following we leave as an exercise for the student. it is a quite straight
forward result.

{\bf Theorem 7:} $\forall x,y\ ((\forall \rho(\neg /occur/[\rho,\ y])) \supset
(/unify/[x,\ y]=/match/[x,\ y,\ \qNIL]))$
\noindent{\bf A more efficient unification program:}

Our program /unify/ can be improved in many ways, the most obvious being
to eliminate the needless task of actually carrying out the substitutions.
The following version is almost identical to our original program except
that it uses {\it virtual substitution} rather than actual.
\medskip
\begindefun
(defun v-unify (x y) (v-uni x y 'nil))
(defun v-uni (x y a)
  (cond ((or (eq a 'no) (eq x y)) a)
        ((and (isvar x) (assoc x a)) (v-uni (cdr (assoc x a)) y a))
        ((and (isvar y) (assoc y a)) (v-uni x (cdr (assoc y a)) a))
        ((isvar x) (if (v-occur x y a) 'no (compose a (cons (cons x y) nil))))
        ((isvar y) (if (v-occur y x a) 'no (compose a (cons (cons y x) nil))))
        ((or (atom x) (atom y)) 'no)
        ( T  (v-uni (cdr x) 
                    (cdr y) 
                    (v-uni (car x) (car y) a)))))
(defun v-occur (x y a)
  (if (and (isvar y) (assoc y a))
      (v-occur x (cdr (assoc y a)) a)
      (if (atom y)
          (eq x y)
          (or (v-occur x (car y) a)
              (v-occur x (cdr y) a)) ) ) )
\enddefun